
#include "NodeParallel.h"
#include "Node.h"
#include <vector>
#include <iostream>
using namespace std;

__device__ inline bool isSolved(NodeParallel node)
{
	return *(node.bitmap) & (1 << 0);
}

__device__ inline bool isSolvable(NodeParallel node)
{
	return *(node.bitmap) & (1 << 1);
}

__device__ inline bool varAffected(NodeParallel node, int i)
{
	return *(node.b1 + i / 8) & (1 << i % 8);
}

__device__ inline bool varValues(NodeParallel node, int i)
{
	return *(node.b2 + i / 8) & (1 << i % 8);
}

__device__ inline bool solvedClauses(NodeParallel node, int i)
{
	return *(node.b3 + i / 8) & (1 << i % 8);
}

__device__ inline bool clauseLiterals(NodeParallel node, int k, int i)
{
	return *(node.b4 + (k + i * node.m) / 8) & (1 << (k + i * node.m) % 8);
}

__device__ inline void set_solved(NodeParallel node, bool val)
{
	if (isSolved(node) != val)
	{
		*(node.bitmap) ^= (1 << 0);
	}
}

__device__ inline void set_solvable(NodeParallel node, bool val)
{
	if (isSolvable(node) != val)
	{
		*(node.bitmap) ^= (1 << 1);
	}
}

__device__ inline void set_varAffected(NodeParallel node, int i, bool val)
{
	if (varAffected(node, i) != val)
	{
		*(node.b1 + i / 8) ^= (1 << i % 8);
	}
}

__device__ inline void set_varValues(NodeParallel node, int i, bool val)
{
	if (varValues(node, i) != val)
	{
		*(node.b2 + i / 8) ^= (1 << i % 8);
	}
}

__device__ inline void set_solvedClauses(NodeParallel node, int i, bool val)
{
	if (solvedClauses(node, i) != val)
	{
		*(node.b3 + i / 8) ^= (1 << i % 8);
	}
}

__device__ inline void set_clauseLiterals(NodeParallel node, int k, int i, bool val)
{
	if (clauseLiterals(node, k, i) != val)
	{
		*(node.b4 + (k + i * node.m) / 8) ^= (1 << (k + i * node.m) % 8);
	}
}

__device__ inline int negation (NodeParallel node, int i)
{
	return 2 * node.n - 1 - i;
}

__device__ NodeParallel buildNode(char *output, size_t * output_nb_unaffected,
								  char *b, size_t * u, int a_n, int a_m)
{
	NodeParallel node;
	node.n = a_n;
	node.m = a_m;
	node.o = 2*a_n*a_m;
	
	size_t memory_n = (a_n % 8 == 0 ? a_n / 8 : a_n / 8 + 1);
	size_t memory_m = (a_m % 8 == 0 ? a_m / 8 : a_m / 8 + 1);
	size_t memory_nm = (2*a_n*a_m % 8 == 0 ? 2*a_n*a_m / 8 : 2*a_n*a_m / 8 + 1);
	
	node.bitmap = output;
	
	node.b1 = node.bitmap + 1;
	node.b2 = node.b1 + memory_n;
	node.b3 = node.b2 + memory_n;
	node.b4 = node.b3 + memory_m;
	
	memcpy(node.bitmap, b, 1 + 2 * memory_n + memory_m + memory_nm);

	node.nb_unaffected = output_nb_unaffected;
	memcpy(node.nb_unaffected, u, node.m * sizeof(size_t));
	
	return(node);
}


__global__ void exploreOneParallel (char* output, size_t * output_nb_unaffected,
									char* b, size_t * u, int *vars, int n,
									int m, int N, size_t allocated_size)
{
	int i = blockIdx.x * blockDim.x + threadIdx.x;
	
	if(i >= (1 << N))
	{
		return;
	}
	
	NodeParallel result = buildNode(output+i*allocated_size,
									output_nb_unaffected + i * m, b, u, n, m);

	//Affect the variables as given by the parameters and the thread's index
	int currentVar;
	bool currentValue;
	bool solvedOneClause = false;
	for (int j = 0; j < N; j++)
	{
		currentVar = vars[j];
		currentValue = (i & (1<<j)) != 0 ? true : false;
		set_varAffected(result, currentVar,true);
		set_varValues(result, currentVar, currentValue);
	}

	for(int k=0; k < m; k++)
	{
		if(!solvedClauses(result, k))
		{
			bool solved = false;

			for (int j = 0; !solved && j < N; j++)
			{
				currentVar = vars[j];
				currentValue = (i & (1<<j)) != 0 ? true : false;

				//If the affectation did not satisfy the clause, we remove the variable
				//from the remaining literals of the clause. If it did, we mark the clause
				//as satisfied
				if(clauseLiterals(result, k, currentVar))
				{
					if(currentValue)
					{
						set_solvedClauses(result, k, true);
						solved = true;
						solvedOneClause = true;
					}
					else
					{
						set_clauseLiterals(result, k, currentVar, false);
						result.nb_unaffected[k]--;
					}
				}
				else if(clauseLiterals(result, k, negation(result, currentVar)))
				{
					if(!currentValue)
					{
						set_solvedClauses(result, k, true);
						solved = true;
						solvedOneClause = true;
					}
					else
					{
						set_clauseLiterals(result, k, negation(result, currentVar), false);
						result.nb_unaffected[k]--;
					}
				}
			}
		}
	}

	//Unit propagation
	bool propagated;
	do
	{
		propagated = false;

		for (int c = 0; c < m; c++)
		{
			if (!solvedClauses(result, c))
			{
				//For each clause, get the number of unaffected literals
				int nb_unaffected = result.nb_unaffected[c];

				//If there are none of them, then the formula isn't solvable
				if (nb_unaffected == 0)
				{
					set_solvable(result, false);
					return;
				}

				//Else, if there's just one of this literal, it must be set to
				//true
				else if (nb_unaffected == 1)
				{
					propagated = true;
					int variable;
					bool value;
					for (int l = 0; l < 2 * n; l++)
					{
						if (clauseLiterals(result, c, l))
						{
							value = l < n;
							variable = value ? l : negation(result, l);
							break;
						}
					}
					set_varAffected(result, variable, true);
					set_varValues(result, variable, value);

					//Each time we affect a variable, we check the unsatisfied clauses containing it
					for(int k=0; k < m; k++)
					{
						if(!solvedClauses(result, k))
						{
							//If the affectation did not satisfy the clause, we remove the variable
							//from the remaining literals of the clause. If it did, we mark the clause
							//as satisfied
							if(clauseLiterals(result, k, variable))
							{
								if (value)
								{
									set_solvedClauses(result, k, true);
									solvedOneClause = true;
								}
								else
								{
									set_clauseLiterals(result, k, variable, false);
									result.nb_unaffected[k]--;
								}
							}
							else if(clauseLiterals(result, k, negation(result, variable)))
							{
								if (!value)
								{
									set_solvedClauses(result, k, true);
									solvedOneClause = true;
								}
								else
								{
									set_clauseLiterals(result, k, negation(result, variable), false);
									result.nb_unaffected[k]--;
								}
							}
						}
					}
				}
			}
		}
	}
	while (propagated);
	
	//If we have satisfied a new clause, we check if the problem is solved
	if(isSolvable(result) && solvedOneClause)
	{
		set_solved(result, true);
		for(int j=0; j < m; j++)
		{
			if(!solvedClauses(result, j))
			{
				set_solved(result, false);
				break;
			}
		}
	}
}

__host__ void testError(int line)
{
	cudaError_t error;
	if((error = cudaGetLastError()) != cudaSuccess)
	{
		cerr<<"Ooops, an error occured (l."<<line<<"): "<<cudaGetErrorString(error)<<endl;
		exit(EXIT_FAILURE);
	}
}

__host__ vector<Node> Node::exploreParallel(unsigned int N)
{
	vector<Node> result;
	
	/* First simplify the current node, if the formula has been satisfied by
	 simplification, just return the current node.
	 */
	if (isSolved())
	{
		result.push_back(*this);
	}
	
	/* Else, branch on the given number of next unaffected variables. */
	else
	{
		unaffected(N);
		
		if(isSolvable())    //If the problem is not solvable, we don't create new nodes
		{
			//We branch on vars.size() binary variables
			int nbNewNodes = 1 << nbSelected;

			//Memory allocation
			char *device_bitmap;
			int *device_vars;
			char *device_output;
			size_t * device_nb_unaffected;
			size_t * device_output_nb_unaffected;
			
			cudaMalloc(&device_bitmap, allocated_size);							testError(__LINE__);
			cudaMalloc(&device_vars, nbSelected*sizeof(int));					testError(__LINE__);
			cudaMalloc(&device_output, nbNewNodes*allocated_size);				testError(__LINE__);
			cudaMalloc(&device_nb_unaffected, m*sizeof(size_t));				testError(__LINE__);
			cudaMalloc(&device_output_nb_unaffected,
					   nbNewNodes*m*sizeof(size_t));				testError(__LINE__);
			
			cudaMemcpy(device_bitmap, bitmap, allocated_size,
					   cudaMemcpyHostToDevice);									testError(__LINE__);
			
			cudaMemcpy(device_vars, selectedVars, nbSelected*sizeof(int),
					   cudaMemcpyHostToDevice);									testError(__LINE__);

			cudaMemcpy(device_nb_unaffected, nb_unaffected, m * sizeof(size_t),
					   cudaMemcpyHostToDevice);
			
			//Function call
			dim3 dimBlock(NB_THREADS_PER_BLOCK);
			dim3 dimGrid(nbNewNodes % dimBlock.x == 0 ?
						 nbNewNodes / dimBlock.x : nbNewNodes / dimBlock.x + 1);

			exploreOneParallel<<<dimGrid, dimBlock>>>
						(device_output, device_output_nb_unaffected,
						 device_bitmap, device_nb_unaffected, device_vars, n, m,
						 nbSelected, allocated_size);
			
			cudaThreadSynchronize();											testError(__LINE__);
			
			
			//Getting back the results
			for(int i=0; i<nbNewNodes; i++)
			{
				Node node(n,m);
				
				cudaMemcpy(node.bitmap, device_output+i*allocated_size, allocated_size,
						   cudaMemcpyDeviceToHost);								testError(__LINE__);
				cudaMemcpy(node.nb_unaffected,
						   device_output_nb_unaffected + i * m,
						   m * sizeof(size_t), cudaMemcpyDeviceToHost);
				
				if(node.isSolvable())
				{
					result.push_back(node);
				}
			}

			//Free allocated memory
			cudaFree(device_bitmap);							testError(__LINE__);
			cudaFree(device_vars);					testError(__LINE__);
			cudaFree(device_output);				testError(__LINE__);
			cudaFree(device_nb_unaffected);				testError(__LINE__);
			cudaFree(device_output_nb_unaffected);				testError(__LINE__);
		}
	}
	
	return(result);
}



